--- 'Nice' instances for types and expressions.
module frege.compiler.instances.Nicer where 

import frege.Prelude hiding (<+>)

import  frege.data.TreeMap as TM(TreeMap, lookup, delete, each, insert, union, including, contains, keys, values, fromKeys)
import  frege.compiler.enums.TokenID(TokenID)
import  frege.compiler.enums.Literals
import  frege.compiler.types.Positions
-- import  frege.compiler.types.Tokens
import  frege.compiler.types.QNames
import  frege.compiler.types.Types
import  frege.compiler.types.Patterns
import  frege.compiler.types.Symbols
import  frege.compiler.types.Expression
import  frege.compiler.types.Global  as  G
import  frege.compiler.classes.QNameMatcher(QNameMatcher)
import  frege.compiler.classes.Nice(Nice)
import  frege.compiler.common.UnAlias
import  frege.compiler.common.Types  as  TU
import  Compiler.enums.Flags
import  Lib.PP(text, </>, <+>, <>)


private showex nicest x global = showprec 17 x where
    optree = empty -- Global.optab global
    pnice pat 
       | nicest    = Pattern.nicer pat global
       | otherwise = Pattern.nice pat global 
    -- showprec :: Int -> ExprT Nice:q -> String
    -- showprec   n (Vbl {pos, name=Local uid v}) | lambdachar=="\\" = v ++ "§" ++ show uid
    showprec   n (Vbl {pos, name})
        | not nicest = sv
        | pos != Position.null && pos.first == pos.last  = pos.first.value
        | pos != Position.null && pos.first.vor pos.last = pos.first.value ++ pos.last.value
        | m ~ ´^Prelude\w*\.(.+)$´ <- sv, Just x <- m.group 1 = x
        | ´\.\[\]$´   <- sv = "[]"
        | ´\.\[\].\:´ <- sv = ":"
        | otherwise = sv
        where
            sv  = if nicest then nicer name global else nice name global


    showprec  n (Con {name,pos,typ}) = showprec  n (Vbl {name,pos,typ})
    showprec  n (lit@Lit{}) = (if lit.negated then "-" else "") ++ lit.value ++
                                (if       lit.kind == LBig then "n"
                                 else if  lit.kind == LDec then "z" else "") 
    showprec  n (Mem x s _) = showprec  0 x ++ "." ++ s.value
    showprec  0 x = "(" ++ showprec  17 x ++ ")"

    showprec  n (App (App fun x1 _) x2 _)
        | Just v <- varcon fun, Just op <- isop (sop v)
            -> let
                  left o  = o >= LOP1 && o <= LOP16
                  right o = o >= ROP1 && o <= ROP16
                  prec o  = if left o then 2+o.ord-TokenID.ord LOP1
                            else if right o then 2+o.ord-TokenID.ord ROP1
                            else 2+o.ord-TokenID.ord NOP1
                  pop = prec op
                  sleft  = if left op  then showprec  pop x1
                                       else showprec  (pop-1) x1
                  sright = if right op then showprec  pop x2
                                       else showprec  (pop-1) x2
            in if n < pop then "(" ++ sleft ++ ops v ++ sright ++ ")"
            else sleft ++ ops v ++ sright
        where {
            varcon (Vbl {name=v}) = Just v;
            varcon (Con {name=v}) = Just v;
            varcon _ = Nothing;
            sop v = showprec 17 fun; -- (Vbl {pos=Position.null, name=v, typ=Nothing});
            ops v = if sop v ~ ´\w´ then " `" ++ sop v ++ "` " else sop v;
            isop x
                | Just this <- TreeMap.lookupS optree x = Just this
                | m ~ ´\.([^\.]+)$´ <- x, Just o <- m.group 1,
                  Just this <- TreeMap.lookupS optree o = Just this
                | x == ":"               = Just ROP13
                | x == "[].:"            = Just ROP13
                | otherwise              = Nothing;
        }


    showprec n (app@App a b _)
        | tu:es <- map fst (flatx app), n <- ntuple tu, length es == n     -- (a,b)
        = "(" ++ joined ", " (map (showprec 17) es) ++ ")"
        | otherwise = showprec 1 a ++ " " ++ showprec 0 b
        where
            {-
             * check if this is a  tuple constructor and return the
             * number of arguments the tuple constructor needs
             * if ntuple x < 2 then this is not a tuple
             -}
            ntuple (Con {name=s})
                | m ~ ´\((,+)\)´ <- nice s global,
                  Just commata <- m.group 1 = 1 + commata.length
                | otherwise                 = 0
            ntuple _ = 0

    showprec 17 (Ifte a b c _) = "if " ++ showprec 17 a ++ " then " ++ showprec 17 b ++ " else " ++ showprec 17 c
    {-showprec 17 (Case CaseWhen  e alts) = "when " ++ showprec 17 e
                                        ++ " of {"
                                        ++ join "; " (map shalt alts)
                                        ++ "}"
                         where {
                   shalt {pat,ex,line=_,env=_} = Pattern.show pat ++ "->" ++ showprec 17 ex;
                }-}
    showprec 17 (Case _ e (a:as) _) = "case " ++ showprec 17 e
                                        ++ " of {"
                                        ++ pnice a.pat ++ "->"
                                        ++ showprec 17 a.ex ++ rest where
             rest | null as = "}"
                  | otherwise = "; ...}"

    showprec 17 (Let kt e _)
        | length kt >  1  = "let " ++ dspl kt ++ " in " ++ showprec 17 e
        | nicest = "let " ++ QName.base (head kt) ++ "=" ++ sv vt ++ " in ..."
        | length kt == 1     = "let " ++ QName.base (head kt) ++ "=" ++ sv vt ++ " in " ++ showprec 17 e
        | otherwise = "let ... in " ++ showprec 17 e  -- Prelude.error "showprec empty let"
        where
            -- kt = keys t
            vt = [ s | k <- kt, s <- global.findit k ]
            sv ((vsym@SymV{}):_)
                | Just x <- vsym.gExpr global = if not nicest
                    then nice x global
                    else nicer x global          -- NOT "showprec 17 x"  as this imposes
                                                 -- a too restricted Expr to showprec
                                                 -- when no annotation prevents it
                | otherwise = "???"
            sv (sym:_) = Prelude.error ("showprec no variable: " ++ sym.nice global)
            sv [] = "?"
            dspl [] = ""
            dspl [x] = QName.base x
            dspl (x:xs) = QName.base x ++ ", " ++ dspl xs

    showprec 17 (Lam p e _)  = "λ" ++ pnice p        -- avoids \u which irritates javac
                                        ++ " -> " ++ showprec 17 e
    showprec n (Ann x (Just t)) = "(" ++ showprec 17 x ++ "::" ++ t.nicer global ++ ")"
    showprec n (Ann x Nothing)  = "(" ++ showprec 17 x ++ "::" ++ "Nothing?" ++ ")"
    showprec n x | n != 17 = showprec 0 x
                 | otherwise = Prelude.error ("can't show expression with constructor " ++ show (constructor x))


instance Nice  ExprT where
    nice  = showex false
    nicer = showex true
    nicest g x | valid = result
               | otherwise = text (nicer x g)
        where
            code = g.sub.code
            p = getrange x
            extract o l = (code.subSeq o (o+l)).toString
            valid = p.first.offset < code.length && p.last.offset + p.last.length <= code.length
                    -- && p.first.value == extract p.first.offset p.first.length
            portion = extract p.first.offset (p.last.offset + p.last.length - p.first.offset)
            result
                | p.first.line < p.last.line  = PP.stack . map text . lines $ portion
                | otherwise = text portion



instance (Nice q, QNameMatcher q) => Nice (PatternT q) where
    nice  p g = showp g false 17 p
    nicer p g = showp g true  17 p


private showp g nicer 0 (PVar {uid,var})
    | nicer     = var
    | otherwise = var ++ "{" ++ show uid ++ "}"
private showp g nicer 0 (PCon {qname}) | qname.nice g ~ ´\[\]$´ = "[]"
private showp g nicer 0 (PCon {qname, pats=[]}) = qname.nicer g
private showp g nicer 0 (PCon {qname, pats}) 
    | qname.nice g ~ ´\(,+\)$´ = "(" ++ joined "," (map (showp g nicer 17) pats) ++ ")"
private showp g nicer 0 (PConFS {qname, fields}) = qname.nicer g ++ "{" ++ sf fields ++ "}"
    where
        sf fs = joined "," (map sf1 fs)
        sf1 (a,p) = a ++ "=" ++ showp g nicer 17 p
private showp g nicer 0 (PLit {kind=LBig, value}) = value ++ "n"
private showp g nicer 0 (PLit {kind=LLong, value}) = value ++ "L"
private showp g nicer 0 (PLit {kind=LFloat, value}) = value ++ "f"
private showp g nicer 0 (PLit {value}) = value
private showp g nicer 0 (PUser p lazy) = (if lazy then "?" else "!") ++ showp g nicer 0 p
private showp g nicer 0 p = "(" ++ showp g nicer 17 p ++ ")"
private showp g nicer 17 (PAnn p t) = showp g nicer 15 p ++ "::" ++ (if nicer then t.nicer g else t.nice g)
private showp g nicer 17 p = showp g nicer 15 p
private showp g nicer 15 (PAt{var,pat}) = var ++ "@" ++ showp g nicer 15 pat
private showp g nicer 15 p = showp g nicer 13 p
private showp g nicer 13 (PCon {qname, pats=[p,ps]}) 
    | qname.nice g ~ ´:$´ = showp g nicer 2 p ++ ":" ++ showp g nicer 13 ps
private showp g nicer 13 p = showp g nicer 2 p
private showp g nicer 2  (PMat{var,value}) = var ++ "~" ++ value
private showp g nicer 2  p = showp g nicer 1 p
private showp g nicer 1  (p@PCon {qname,pats})
    | null pats || qname.nice g ~ ´\(,+\)$´ = showp g nicer 0 p
private showp g nicer 1  (PCon {qname, pats}) = qname.nice g ++ " " ++ joined " " (map (showp g nicer 0) pats)
private showp g nicer 1  p = showp g nicer 0 p
private showp g nicer _  p = Prelude.error ("can't show pattern with constructor" ++ show (constructor p))


instance (Nice t, QNameMatcher t) => Nice (SigmaT t) where
    nice (sig@ForAll bndrs rho) g 
        | null bndrs = rho.nice g
        | otherwise  = fA ++ vars ++ "." ++ rho.nice g
        where
            fA = if isOn g.options.flags USEUNICODE then "∀ " else "forall "
            vars = joined " " . map (flip nice g) . _.tvars  $ sig 
    nicer (sig@ForAll bndrs rho) g 
        | null bndrs = rho.nicer g
        | otherwise  = fA ++ vars ++ "." ++ rho.nicer g
        where
            fA = if isOn g.options.flags USEUNICODE then "∀ " else "forall "
            vars = joined " " . map (flip nicer g) . _.tvars $ sig

instance (Nice t, QNameMatcher t) => Nice (RhoT t) where
    nice (RhoFun ctx sigma rho) g
        | ForAll (_:_) _ <- sigma = nicectx ctx g ++ "(" ++ sigma.nice g ++ ") " ++ arrow ++ " " ++ rng
        | isFun sigma g           = nicectx ctx g ++ "(" ++ sigma.nice g ++ ") " ++ arrow ++ " " ++ rng
        | otherwise               = nicectx ctx g ++ sigma.nice g        ++  " " ++ arrow ++ " " ++ rng
        where
            arrow = if isOn g.options.flags USEUNICODE then "→" else "->"
            !rng = rho.{context=[]}.nice g
    nice (RhoTau ctx tau) g       = nicectx ctx g ++ tau.nice g
    nicer (RhoFun ctx sigma rho) g
        | ForAll (_:_) _ <- sigma = nicerctx ctx g ++ "(" ++ sigma.nicer g ++ ") " ++ arrow ++ " " ++ rng
        | isFun sigma g           = nicerctx ctx g ++ "(" ++ sigma.nicer g ++ ") " ++ arrow ++ " " ++ rng
        | otherwise               = nicerctx ctx g ++ sigma.nicer g        ++  " " ++ arrow ++ " " ++ rng
        where
            arrow = if isOn g.options.flags USEUNICODE then "→" else "->"
            !rng = rho.{context=[]}.nicer g
    nicer (RhoTau ctx tau) g      = nicerctx ctx g ++ tau.nicer g


nicectx :: (Nice t, QNameMatcher t) => [ContextT t] -> Global -> String
nicectx [] g = ""
nicectx xs g
    | [ctx] <- xs = single ctx ++ arrow
    | otherwise   = "(" ++ joined "," (map single xs) ++ ")" ++ arrow
    where
        arrow = if isOn g.options.flags USEUNICODE then " ⇒ " else " => "
        single (Ctx pos name tau) = nice (TApp (TCon {pos,name}) tau) g


nicerctx :: (Nice t, QNameMatcher t) => [ContextT t] -> Global -> String
nicerctx [] g = ""
nicerctx xs g
    | [ctx] <- xs = single ctx ++ arrow
    | otherwise   = "(" ++ joined "," (map single xs) ++ ")" ++ arrow
    where
        arrow = if isOn g.options.flags USEUNICODE then " ⇒ " else " => "
        single (Ctx pos name tau) = nicer (TApp (TCon {pos,name}) tau) g


instance (Nice t, QNameMatcher t) => Nice (TauT t) where
    nicer t g = showt 2 (unAlias g t) -- if isOn g.options.flags IDE then showt 2 (unAlias g t) else nice t g
        where
            arrow = if isOn g.options.flags USEUNICODE then "→" else "->"
            showt 2 fun
                | [TCon {name}, a, b] <- Tau.flat fun,
                  name.nice g ~ ´(->|→)$´
                                 = showt 1 a ++ arrow ++ showt 2 b
            showt 2 (TSig s)     = nicer s g
            showt 2 x            = showt 1 x
            showt _ (t@TApp _ _)
                | [TCon {name}, t] <- flat, name.nice g ~ ´\[\]$´ = "[" ++ showt 2 t ++ "]"
                | (TCon {name}:ts) <- flat, name.nice g ~ ´\(,+\)$´ = "(" ++ joined "," (map (showt 2) ts) ++ ")"
                | isEither flat = "(" ++ showEither flat ++ ")"
                where 
                    flat = t.flat
                    isEither [TCon{name}, a, b] = name.nice g ~ ´\bEither$´
                    isEither _ = false
                    showEither [_, a, b]
                        | TApp{} <- a, isEither aflat = showEither aflat ++ " | " ++ showt 2 b
                        | otherwise =  showt 2 a ++ " | " ++ showt 2 b
                        where aflat = Tau.flat a
                    showEither _ = Prelude.error ("only good for Either a b")
            showt 1 fun
                | [TCon {name}, a, b] <- Tau.flat fun,
                  name.nice g ~ ´(->|→)$´
                                  = "(" ++ showt 1 a ++ arrow ++ showt 2 b ++ ")"
            showt 1 (TApp a b)    = showt 1 a ++ " " ++ showt 0 b
            showt 1 x             = showt 0 x
            showt 0 (tv@TVar {var})
                | bs ← tv.bounds, not (null bs) = case tv.wildTau of
                    Just "<" →  "(≤" ++ manyK g nicer bs ++ ")"
                    Just ">" →  "(≥" ++ manyK g nicer bs ++ ")"
                    _        →  "(" ++ var ++ "≤" ++ manyK g nicer bs ++ ")"
                | otherwise  = var
            showt 0 (Meta tv)     = tv.nicer g
            showt 0 (TCon {name}) = name.nicer g
            showt _ x             = "(" ++ showt 2 x ++ ")"
    nice t g = showt 2 t
        where
            arrow = if isOn g.options.flags USEUNICODE then "→" else "->"
            showt 2 fun
                | [TCon {name}, a, b] <- Tau.flat fun,
                  name.nice g ~ ´->|→$´
                                  = showt 1 a ++ arrow ++ showt 2 b
            showt 2 (TSig s)      = nice s g
            showt 2 x             = showt 1 x
            showt _ (t@TApp _ _)
                | [TCon {name}, t] <- flat, name.nice g ~ ´\[\]$´ = "[" ++ showt 2 t ++ "]"
                | (TCon {name}:ts) <- flat, name.nice g ~ ´\(,+\)$´ = "(" ++ joined "," (map (showt 2) ts) ++ ")"
                where flat = t.flat
            showt 1 fun
                | [TCon {name}, a, b] <- Tau.flat fun,
                  name.nice g ~ ´(->|→)$´                                  = "(" ++ showt 1 a ++ arrow ++ showt 2 b ++ ")"
            showt 1 (TApp a b)    = showt 1 a ++ " " ++ showt 0 b
            showt 1 x             = showt 0 x
            showt 0 (tv@TVar {var})
                | bs ← tv.bounds, not (null bs) = case tv.wildTau of
                    Just "<" →  "(≤" ++ manyK g nice bs ++ ")"
                    Just ">" →  "(≥" ++ manyK g nice bs ++ ")"
                    _        →  "(" ++ var ++ "≤" ++ manyK g nice bs ++ ")"
                | otherwise  = var

            showt 0 (Meta tv)     = tv.nice g
            showt 0 (TCon {name}) = name.nice g
            showt 0 x             = "(" ++ showt 2 x ++ ")"
            showt _ x             = Prelude.error ("can't show type with constructor " ++ show (constructor x))

instance Nice Kind where
    nice KType g = "*"
    nice (KGen ts) g = manyK g nice  ts 
    nice KVar  g = "?"
    nice (KApp k1 k2) g
        | KApp{} ← k1  = "(" ++ nice k1 g ++ ") -> " ++ nice k2 g
        | otherwise    = nice k1 g ++ " -> " ++ nice k2 g
    nicer KType g = "*"
    nicer (KGen ts) g = manyK g nicer  ts
    nicer KVar  g = "?"
    nicer (KApp k1 k2) g
        | KApp{} ← k1  = "(" ++ nice k1 g ++ ") -> " ++ nice k2 g
        | otherwise    = nice k1 g ++ " -> " ++ nice k2 g

manyK g f = joined ", " . map (\k -> f k g)

instance (Nice s, QNameMatcher s) => Nice (MetaTvT s) where
    nice (rigid@Rigid i s _) g = case (Meta rigid).bounds of
        []       → "t" ++ show i ++ "#" ++ s
        bs       → case (Meta rigid).wildTau of
            Just "<" → "(?" ++ nice rigid.{kind=KType::Kind} g ++ "≤" ++ manyK g nice bs ++ ")"
            Just ">" → "(?" ++ nice rigid.{kind=KType::Kind} g ++ "≥" ++ manyK g nice bs ++ ")"
            _        → "("  ++ nice rigid.{kind=KType::Kind} g ++ "≤" ++ manyK g nice bs ++ ")"
        
    nice (flexi@Flexi{uid, hint, kind}) g
        | Just t <- g.bound flexi = "<" ++ t.nice g.{tySubst ← delete uid} ++ ">"
        | bs ← (Meta flexi).bounds, not (null bs) = case (Meta flexi).wildTau of
                    Just "<" →  "<?" ++ show uid ++ "≤" ++ manyK g nice bs ++ ">"
                    Just ">" →  "<?" ++ show uid ++ "≥" ++ manyK g nice bs ++ ">"
                    _        →  "<" ++ show uid ++ " " ++ hint ++ "≤" ++ manyK g nice bs ++ ">"
        | otherwise          =  "<" ++ show uid ++ " " ++ hint ++ ">"
        
    nicer (rigid@Rigid i s _) g = case (Meta rigid).bounds of
        []  → {- "t" ++ show i ++ "#" ++ -} s
        bs  → case (Meta rigid).wildTau of
            Just "<" → "(?" ++ nicer rigid.{kind=KType::Kind} g ++ "≤" ++ manyK g nicer bs ++ ")"
            Just ">" → "(?" ++ nicer rigid.{kind=KType::Kind} g ++ "≥" ++ manyK g nicer bs ++ ")"
            _        → "("  ++ nicer rigid.{kind=KType::Kind} g ++ "≤" ++ manyK g nicer bs ++ ")"
        
    nicer (flexi@Flexi{uid, hint, kind}) g
        | Just t <- g.bound flexi = t.nicer g.{tySubst ← delete uid}
        | bs ← (Meta flexi).bounds, not (null bs) = case (Meta flexi).wildTau of
                    Just "<" →  "(?" ++ show uid ++ "≤" ++ manyK g nicer bs ++ ")"
                    Just ">" →  "(?" ++ show uid ++ "≥" ++ manyK g nicer bs ++ ")"
                    _        →  "(t" ++ show uid ++ "≤" ++ manyK g nicer bs ++ ")"
        | otherwise          =  "t" ++ show uid
